/*
Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. This file is part of NESCOND.NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see <http://www.gnu.org/licenses/>.
*/

/* imports */
:- use_module(library(lists)).
:- use_module(operators).

/* A nested sequent Gamma is a Prolog list of the form:

   Gamma = [F_1, F_2, ..., F_m, [[A_1,Gamma_1],AppliedConditionals_1], [[A_2,Gamma_2],AppliedConditionals_2], ..., [[A_n,Gamma_n],AppliedConditionals_n]]  ]

   where F_i are formulas of the conditional language, A_i are formulas of the conditional language and Gamma_i are Prolog lists representing nested sequents.

  --------------------------------------------------------------------------------------------------------------------------------------------------------------

   A context is a triple [Context,AppliedConditionals,AllowID] where:
   - Context has the form [Fml,Gamma], where Fml is a formula of the conditional language and Gamma is a Prolog list representing a nested sequent
   - AppliedConditionals is a Prolog list [A_1=>B_1,A_2=>B_2,...,A_k=>B_k]
   such that the rule (=>-) has been already applied to each formula in AppliedConditionals by using Context.
   - AllowID is a boolean element. When AllowID is true, then the rule (ID) can bu applied to that context in a backward proof
     search. When AllowID is false, (ID) has already been applied to id, therefore the rule is no longer applicable to that context.
   
   Example: [[A,Gamma],[B=>C,D=>E],false] means that (=>-) has been already applied to 
      B=>C and D=>E with [A:Gamma] in the current branch, and that (ID) has been already 
     applied to [A:Gamma] in the current branch.

   The last two elements are used in order to ensure the termination of the calculi.


*/


fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!,
								  append(TempNS,ListToFill,NewNS).
fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals,AllowID]|TempNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,TempNS),
								  fillTheHole(Gamma,ListToFill,NewGamma).

selectList([],NS,[hole|NS]).
selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS),
								 selectList(Tail,TempNS,NewNS).
						
deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS).
deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals,AllowID]|NewNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,NewNS),
						   deepSelect(List,Gamma,NewGamma).

memberList([],_).
memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS).
deepMember(List,NS):-memberList(List,NS).
deepMember(List,NS):-member([[_,Gamma],_,_],NS),
					 deepMember(List,Gamma).



/* Axioms closing branches */
prove(NS,_,tree(ax)):-deepMember([P,!P],NS),!.
prove(NS,_,tree(axt)):-deepMember([top],NS),!.
prove(NS,_,tree(axb)):-deepMember([!bot],NS),!.
/* Rules with one premise */
prove(NS,AppliedMP,tree(neg,A,SubTree)):-deepSelect([!!A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),prove(DefNS,AppliedMP,SubTree).
prove(NS,AppliedMP,tree(orp,A,B,SubTree)):-deepSelect([A v B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),prove(DefNS,AppliedMP,SubTree).
prove(NS,AppliedMP,tree(andn,A,B,SubTree)):-deepSelect([!(A ^ B)],NS,NewNS),!,fillTheHole(NewNS,[!A,!B],DefNS),prove(DefNS,AppliedMP,SubTree).
prove(NS,AppliedMP,tree(impp,A,B,SubTree)):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[!A,B],DefNS),prove(DefNS,AppliedMP,SubTree).
prove(NS,AppliedMP,tree(condp,A,B,SubTree)):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[],true]],DefNS),prove(DefNS,AppliedMP,SubTree).
prove(NS,AppliedMP,tree(id,A,SubTree)):-deepSelect([[[A,Delta],AppliedConditionals,true]],NS,NewNS),!,
      fillTheHole(NewNS,[[[A,[!A|Delta]],AppliedConditionals,false]],DefNS),prove(DefNS,AppliedMP,SubTree).
/* Rules with two or three premises (introducing a branch in a backward proof search) */
prove(NS,AppliedMP,tree(orn,A,B,Sub1,Sub2)):-deepSelect([!(A v B)],NS,NewNS),!,fillTheHole(NewNS,[!A],NS1),fillTheHole(NewNS,[!B],NS2),prove(NS1,AppliedMP,Sub1),prove(NS2,AppliedMP,Sub2).
prove(NS,AppliedMP,tree(andp,A,B,Sub1,Sub2)):-deepSelect([A ^ B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),prove(NS1,AppliedMP,Sub1),prove(NS2,AppliedMP,Sub2).
prove(NS,AppliedMP,tree(impn,A,B,Sub1,Sub2)):-deepSelect([!(A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[!B],NS2),prove(NS1,AppliedMP,Sub1),prove(NS2,AppliedMP,Sub2).
prove(NS,AppliedMP,tree(mp,A,B,Sub1,Sub2)):-deepSelect([!(A => B)],NS,NewNS),
    \+member(A => B,AppliedMP),!,
    fillTheHole(NewNS,[A,!(A => B)],NS1),
    fillTheHole(NewNS,[!B,!(A => B)],NS2),
    prove(NS1,[A => B|AppliedMP],Sub1),
    prove(NS2,[A => B|AppliedMP],Sub2).
prove(NS,AppliedMP,tree(condn,A,B,Sub1,Sub2,Sub3)):-
	    deepSelect([!(A => B),[[C,Delta],AppliedConditionals,AllowID]],NS,NewNS),
	    \+member(!(A => B),AppliedConditionals),
	    prove([A,!C],[],Sub2),
	    prove([C,!A],[],Sub3),!,
	    fillTheHole(NewNS,[!(A => B),[[C,[!B|Delta]],[!(A => B)|AppliedConditionals],AllowID]],DefNS),
	    prove(DefNS,AppliedMP,Sub1).